k:Knd, T, B:Type, l:IdLnk, ds:x:Id fp Type, tg:Id, f:(State(ds)TB).
(isrcv(k)  destination(lnk(k)) = source(l)  Id & (lnk(k) = l  T = B & tag(k) = tg))
 Normal(ds)
 Normal(T)
 Normal(B)
 es.usends1-p(es;ds;k;T;l;tg;B;f) 

latex

Definitions	x:A. B(x), P  Q, P & Q, es.P(es), x:A. B(x), t  T, x. t(x), DeclaredType(ds;x), Top, Prop, x(s)
Lemmas	fpf-single wf, Rsends wf, fpf-cap-single1, id-deq wf, decl-type wf, R-usends1-rule, R-realizes wf, usends1-p wf, event system wf, normal-type wf, normal-ds wf, assert wf, isrcv wf, Id wf, ldst wf, lnk wf, lsrc wf, IdLnk wf, tagof wf, decl-state wf, fpf wf, Knd wf